-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

import "LangPrelude.prg"


exclude :: Tag ~> Row Tag * ~> Row Tag *
{exclude o {}r} = {}r
{exclude a {a=v; r}r} = {exclude a r}
{exclude b {a=v; r}r} = {a=v; {exclude b r}}r

{-

strip :: Nat ~> Row Nat Nat ~> Nat ~> Row Nat Nat
{strip a RNil n} = RNil
{strip a (RCons Z m r) Z} = {strip Z r a}
{strip a (RCons Z m r) (S n)} = RCons a m {strip Z r {plus a (S n)}}
{strip a (RCons (S n) m r) Z} = RCons {plus a (S n)} m {strip Z r a}
{strip a (RCons (S n) m r) (S n')} = {strip (S a) (RCons n m r) n'}

-}

data SingleLabel :: Row Tag * ~> * where
  None :: SingleLabel RNil
  -- {- "not prop" -}More :: ({exclude rest l} == rest) => Label l -> t -> SingleLabel rest -> SingleLabel {l=t;rest}r
  More :: Equal {exclude l rest} rest => Label l -> t -> SingleLabel rest -> SingleLabel {l=t;rest}r
 deriving Record(s)

t1 :: SingleLabel {`a=Int}r
t1 = {`a=25}s

##test "not solvable"
 t2 = {`a=25;undefined}s

t3 = {`a=25,`b=42}s

##test "duplicate tags"
 t4 = {`a=25,`a=25}s



-- Some basic operations on SingleLabel records:
------------------------------------------------

--- separate the head of the record and assemble it again after that.

-- SEE: issue46
apart :: SingleLabel row -> exists a v tail . Maybe ((Label a, v, SingleLabel tail), Equal {a=v; tail}r row, Equal {exclude a tail} tail)
apart {}s = Ex Nothing
apart {l=v; rest}s = Ex (Just ((l, v, rest), Eq, Eq))

-- SEE: issue48
join :: Label a -> v -> SingleLabel tail -> Equal {exclude a tail} tail -> SingleLabel {a=v; tail}r
join a v t Eq = {a=v; t}s

##test "duplicate labels"
  t5 = join `a 42 {`a="GGG"}s Eq

-- this should be accepted
t6 = join `a 42 {`b="GGG"}s Eq


-- deriving evidence

free :: Label a -> SingleLabel r -> Maybe (Equal {exclude a r} r)
free _ {}s = Just Eq
free a {head=v;tail}s = case labelEq a head of
                        Just Eq -> Nothing
                        Nothing -> case free a tail of
                                   Just ev -> check (Just Eq) where theorem ev
                                   Nothing -> Nothing

{- STILL TOO HARD FOR ME
-- pulling stuff to front

{-
toFront :: Label a -> SingleLabel row -> (SingleLabel {a=v; {exclude a row}}r + SingleLabel {exclude a row})
toFront a (e@{}s) = R e
toFront a (got@{f=v; rest}s) = case labelEq a f of
			       Nothing -> case toFront a rest of
					  R free -> R {f=v; free}s
					  L {a'=v; rest'}s -> L {a'=v', f=v; rest'}s
			       Just Eq -> L got
-}

extendLemma :: Label l -> Equal a b -> Equal {exclude l a} {exclude l b}
extendLemma l Eq = Eq

-- unsound:
--contractLemma :: Label l -> Equal {exclude l a} {exclude l b} -> Equal a b
--contractLemma l Eq = Eq

idempotenceLemma :: Label l -> Equal {exclude l a} b -> Equal {exclude l {exclude l a}} b
idempotenceLemma l Eq = undefined -- Eq CHEAT

idempotenceLemma' :: Label l -> SingleLabel {exclude l a} -> SingleLabel b -> Equal {exclude l a} b -> Equal {exclude l {exclude l a}} b
idempotenceLemma' l s sb Eq = undefined -- Eq CHEAT


------but, the current refinement fails because _c != {exclude _b _c}   vvvvvvvvvvvv
--peel :: Label a -> Equal row {exclude a row} -> SingleLabel {exclude a row} -> SingleLabel row
--peel a Eq s = s

peel :: Label a -> Equal {exclude a row} b -> SingleLabel {exclude a row} -> SingleLabel b
peel a Eq s = s

toFront :: Label a -> SingleLabel row -> (SingleLabel {a=v; {exclude a row}}r + (SingleLabel {exclude a row}, Equal {exclude a row} row))
toFront a (e@{}s) = R (e, Eq)
toFront a (got@{f=v; rest}s) = case labelEq a f of
			       Nothing -> case toFront a rest of
					  --R (free, (t@Eq)) -> R (check {f=v; free}s, Eq) where theorem t, idem = idempotenceLemma' f
                                          --R (free, (t@Eq)) -> R (got, Eq)
                                          R (free, (t@Eq)) -> R (peel f t got, Eq)
					  L {a'=v'; rest'}s -> L {a'=v', f=v; rest'}s
			       Just Eq -> L got

-}
